

LEMMA

External connection implies connection.
=============================
Step 1

? (all x (all y ((ec x y) => (c x y))))


> revsk
=============================
Step 2

? ((~ (ec c663201 c663200)) v (c c663201 c663200))


> hypdisj
=============================
Step 3

? (c c663201 c663200)

1. (ec c663201 c663200)

> ((c X Y) <-- (ec X Y))
=============================
Step 4

? (ec c663201 c663200)

1. (~ (c c663201 c663200))
2. (ec c663201 c663200)

> hyp


LEMMA

Proper part implies parthood.
=============================
Step 1

? (all x (all y ((pp x y) => (p x y))))


> revsk
=============================
Step 2

? ((~ (pp c668330 c668329)) v (p c668330 c668329))


> hypdisj
=============================
Step 3

? (p c668330 c668329)

1. (pp c668330 c668329)

> ((p X Y) <-- (pp X Y))
=============================
Step 4

? (pp c668330 c668329)

1. (~ (p c668330 c668329))
2. (pp c668330 c668329)

> hyp


LEMMA

Tangential proper part implies proper part.
=============================
Step 1

? (all x (all y ((tpp x y) => (pp x y))))


> revsk
=============================
Step 2

? ((~ (tpp c673515 c673514)) v (pp c673515 c673514))


> hypdisj
=============================
Step 3

? (pp c673515 c673514)

1. (tpp c673515 c673514)

> ((pp X Y) <-- (tpp X Y))
=============================
Step 4

? (tpp c673515 c673514)

1. (~ (pp c673515 c673514))
2. (tpp c673515 c673514)

> hyp


LEMMA

Non-tangential proper part implies proper part.
=============================
Step 1

? (all x (all y ((ntpp x y) => (pp x y))))


> revsk
=============================
Step 2

? ((~ (ntpp c678756 c678755)) v (pp c678756 c678755))


> hypdisj
=============================
Step 3

? (pp c678756 c678755)

1. (ntpp c678756 c678755)

> ((pp X Y) <-- (ntpp X Y))
=============================
Step 4

? (ntpp c678756 c678755)

1. (~ (pp c678756 c678755))
2. (ntpp c678756 c678755)

> hyp


LEMMA

Parthood lifts connection from part to whole.
=============================
Step 1

? (all x (all y (all z (((p x y) & (c z x)) => (c z y)))))


> revsk
=============================
Step 2

? (((~ (p c684055 c684054)) v (~ (c c684053 c684055))) v (c c684053 c684054))


> hypdisj
=============================
Step 3

? (c c684053 c684054)

1. (c c684053 c684055)
2. (p c684055 c684054)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var24 c684054)
|
|1. (~ (c c684053 c684054))
|2. (c c684053 c684055)
|3. (p c684055 c684054)
|
|> hyp
=============================
Step 5

? (c c684053 c684055)

1. (~ (c c684053 c684054))
2. (c c684053 c684055)
3. (p c684055 c684054)

> hyp


LEMMA

If x is externally connected to y and y is disconnected from z, then x is not part of z.
=============================
Step 1

? (all x (all y (all z (((ec x y) & (dc y z)) => (~ (p x z))))))


> revsk
=============================
Step 2

? (((~ (ec c689510 c689509)) v (~ (dc c689509 c689508))) v (~ (p c689510 c689508)))


> hypdisj
=============================
Step 3

? (~ (p c689510 c689508))

1. (dc c689509 c689508)
2. (ec c689510 c689509)

> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
|=============================
|Step 4
|
|? (c Var30 c689510)
|
|1. (p c689510 c689508)
|2. (dc c689509 c689508)
|3. (ec c689510 c689509)
|
|> ((c Y X) <-- (c X Y))
|=============================
|Step 5
|
|? (c c689510 Var30)
|
|1. (~ (c Var30 c689510))
|2. (p c689510 c689508)
|3. (dc c689509 c689508)
|4. (ec c689510 c689509)
|
|> ((c X Y) <-- (ec X Y))
|=============================
|Step 6
|
|? (ec c689510 Var30)
|
|1. (~ (c c689510 Var30))
|2. (~ (c Var30 c689510))
|3. (p c689510 c689508)
|4. (dc c689509 c689508)
|5. (ec c689510 c689509)
|
|> hyp
=============================
Step 7

? (~ (c c689509 c689508))

1. (p c689510 c689508)
2. (dc c689509 c689508)
3. (ec c689510 c689509)

> ((~ (c X Y)) <-- (dc X Y))
=============================
Step 8

? (dc c689509 c689508)

1. (c c689509 c689508)
2. (p c689510 c689508)
3. (dc c689509 c689508)
4. (ec c689510 c689509)

> hyp


LEMMA

Case split on whether x is connected to z; if not, then dc x z.
=============================
Step 1

? (all x (all y (all z (((ec x y) & (dc y z)) => ((dc x z) v (c x z))))))


> revsk
=============================
Step 2

? (((~ (ec c695121 c695120)) v (~ (dc c695120 c695119))) v ((dc c695121 c695119) v (c c695121 c695119)))


> hypdisj
=============================
Step 3

? (c c695121 c695119)

1. (~ (dc c695121 c695119))
2. (dc c695120 c695119)
3. (ec c695121 c695120)

> ((c X Y) <-- (~ (dc X Y)))
=============================
Step 4

? (~ (dc c695121 c695119))

1. (~ (c c695121 c695119))
2. (~ (dc c695121 c695119))
3. (dc c695120 c695119)
4. (ec c695121 c695120)

> hyp


LEMMA

If x is connected to z, split on overlap to get ec x z or o x z.
=============================
Step 1

? (all x (all y (all z ((((ec x y) & (dc y z)) & (c x z)) => ((ec x z) v (o x z))))))


> revsk
=============================
Step 2

? ((((~ (ec c700998 c700997)) v (~ (dc c700997 c700996))) v (~ (c c700998 c700996))) v ((ec c700998 c700996) v (o c700998 c700996)))


> hypdisj
=============================
Step 3

? (o c700998 c700996)

1. (~ (ec c700998 c700996))
2. (c c700998 c700996)
3. (dc c700997 c700996)
4. (ec c700998 c700997)

> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|=============================
|Step 4
|
|? (c c700998 c700996)
|
|1. (~ (o c700998 c700996))
|2. (~ (ec c700998 c700996))
|3. (c c700998 c700996)
|4. (dc c700997 c700996)
|5. (ec c700998 c700997)
|
|> hyp
=============================
Step 5

? (~ (ec c700998 c700996))

1. (~ (o c700998 c700996))
2. (~ (ec c700998 c700996))
3. (c c700998 c700996)
4. (dc c700997 c700996)
5. (ec c700998 c700997)

> hyp


LEMMA

If x overlaps z and x is not part of z, then either po x z or pp-1 x z.
=============================
Step 1

? (all x (all y (all z (((((ec x y) & (dc y z)) & (c x z)) & (o x z)) => ((po x z) v (pp-1 x z))))))


> revsk
=============================
Step 2

? (((((~ (ec c707291 c707290)) v (~ (dc c707290 c707289))) v (~ (c c707291 c707289))) v (~ (o c707291 c707289))) v ((po c707291 c707289) v (pp-1 c707291 c707289)))


> hypdisj
=============================
Step 3

? (pp-1 c707291 c707289)

1. (~ (po c707291 c707289))
2. (o c707291 c707289)
3. (c c707291 c707289)
4. (dc c707290 c707289)
5. (ec c707291 c707290)

> ((pp-1 Y X) <-- (pp X Y))
=============================
Step 4

? (pp c707289 c707291)

1. (~ (pp-1 c707291 c707289))
2. (~ (po c707291 c707289))
3. (o c707291 c707289)
4. (c c707291 c707289)
5. (dc c707290 c707289)
6. (ec c707291 c707290)

> ((pp Y X) <-- (p Y X) (~ (p X Y)))
|=============================
|Step 5
|
|? (p c707289 c707291)
|
|1. (~ (pp c707289 c707291))
|2. (~ (pp-1 c707291 c707289))
|3. (~ (po c707291 c707289))
|4. (o c707291 c707289)
|5. (c c707291 c707289)
|6. (dc c707290 c707289)
|7. (ec c707291 c707290)
|
|> ((p Y X) <-- (p X Y) (~ (pp X Y)))
||=============================
||Step 6
||
||? (p c707291 c707289)
||
||1. (~ (p c707289 c707291))
||2. (~ (pp c707289 c707291))
||3. (~ (pp-1 c707291 c707289))
||4. (~ (po c707291 c707289))
||5. (o c707291 c707289)
||6. (c c707291 c707289)
||7. (dc c707290 c707289)
||8. (ec c707291 c707290)
||
||> ((p X Y) <-- (o X Y) (~ (p Y X)) (~ (po X Y)))
||||=============================
||||Step 7
||||
||||? (o c707291 c707289)
||||
||||1. (~ (p c707291 c707289))
||||2. (~ (p c707289 c707291))
||||3. (~ (pp c707289 c707291))
||||4. (~ (pp-1 c707291 c707289))
||||5. (~ (po c707291 c707289))
||||6. (o c707291 c707289)
||||7. (c c707291 c707289)
||||8. (dc c707290 c707289)
||||9. (ec c707291 c707290)
||||
||||> hyp
|||=============================
|||Step 8
|||
|||? (~ (p c707289 c707291))
|||
|||1. (~ (p c707291 c707289))
|||2. (~ (p c707289 c707291))
|||3. (~ (pp c707289 c707291))
|||4. (~ (pp-1 c707291 c707289))
|||5. (~ (po c707291 c707289))
|||6. (o c707291 c707289)
|||7. (c c707291 c707289)
|||8. (dc c707290 c707289)
|||9. (ec c707291 c707290)
|||
|||> hyp
||=============================
||Step 9
||
||? (~ (po c707291 c707289))
||
||1. (~ (p c707291 c707289))
||2. (~ (p c707289 c707291))
||3. (~ (pp c707289 c707291))
||4. (~ (pp-1 c707291 c707289))
||5. (~ (po c707291 c707289))
||6. (o c707291 c707289)
||7. (c c707291 c707289)
||8. (dc c707290 c707289)
||9. (ec c707291 c707290)
||
||> hyp
|=============================
|Step 10
|
|? (~ (pp c707291 c707289))
|
|1. (~ (p c707289 c707291))
|2. (~ (pp c707289 c707291))
|3. (~ (pp-1 c707291 c707289))
|4. (~ (po c707291 c707289))
|5. (o c707291 c707289)
|6. (c c707291 c707289)
|7. (dc c707290 c707289)
|8. (ec c707291 c707290)
|
|> ((~ (pp X Y)) <-- (~ (p X Y)))
|=============================
|Step 11
|
|? (~ (p c707291 c707289))
|
|1. (pp c707291 c707289)
|2. (~ (p c707289 c707291))
|3. (~ (pp c707289 c707291))
|4. (~ (pp-1 c707291 c707289))
|5. (~ (po c707291 c707289))
|6. (o c707291 c707289)
|7. (c c707291 c707289)
|8. (dc c707290 c707289)
|9. (ec c707291 c707290)
|
|> ((~ (p X Z)) <-- (ec X Y) (dc Y Z))
||=============================
||Step 12
||
||? (ec c707291 Var55)
||
||1. (p c707291 c707289)
||2. (pp c707291 c707289)
||3. (~ (p c707289 c707291))
||4. (~ (pp c707289 c707291))
||5. (~ (pp-1 c707291 c707289))
||6. (~ (po c707291 c707289))
||7. (o c707291 c707289)
||8. (c c707291 c707289)
||9. (dc c707290 c707289)
||10. (ec c707291 c707290)
||
||> hyp
|=============================
|Step 13
|
|? (dc c707290 c707289)
|
|1. (p c707291 c707289)
|2. (pp c707291 c707289)
|3. (~ (p c707289 c707291))
|4. (~ (pp c707289 c707291))
|5. (~ (pp-1 c707291 c707289))
|6. (~ (po c707291 c707289))
|7. (o c707291 c707289)
|8. (c c707291 c707289)
|9. (dc c707290 c707289)
|10. (ec c707291 c707290)
|
|> hyp
=============================
Step 14

? (~ (p c707291 c707289))

1. (~ (pp c707289 c707291))
2. (~ (pp-1 c707291 c707289))
3. (~ (po c707291 c707289))
4. (o c707291 c707289)
5. (c c707291 c707289)
6. (dc c707290 c707289)
7. (ec c707291 c707290)

> ((~ (p X Z)) <-- (ec X Y) (dc Y Z))
|=============================
|Step 15
|
|? (ec c707291 Var60)
|
|1. (p c707291 c707289)
|2. (~ (pp c707289 c707291))
|3. (~ (pp-1 c707291 c707289))
|4. (~ (po c707291 c707289))
|5. (o c707291 c707289)
|6. (c c707291 c707289)
|7. (dc c707290 c707289)
|8. (ec c707291 c707290)
|
|> hyp
=============================
Step 16

? (dc c707290 c707289)

1. (p c707291 c707289)
2. (~ (pp c707289 c707291))
3. (~ (pp-1 c707291 c707289))
4. (~ (po c707291 c707289))
5. (o c707291 c707289)
6. (c c707291 c707289)
7. (dc c707290 c707289)
8. (ec c707291 c707290)

> hyp


LEMMA

Converse proper part decomposes into tangential or non-tangential converse proper part.
=============================
Step 1

? (all x (all y ((pp-1 x y) => ((tpp-1 x y) v (ntpp-1 x y)))))


> revsk
=============================
Step 2

? ((~ (pp-1 c714194 c714193)) v ((tpp-1 c714194 c714193) v (ntpp-1 c714194 c714193)))


> hypdisj
=============================
Step 3

? (ntpp-1 c714194 c714193)

1. (~ (tpp-1 c714194 c714193))
2. (pp-1 c714194 c714193)

> ((ntpp-1 Y X) <-- (ntpp X Y))
=============================
Step 4

? (ntpp c714193 c714194)

1. (~ (ntpp-1 c714194 c714193))
2. (~ (tpp-1 c714194 c714193))
3. (pp-1 c714194 c714193)

> ((ntpp Z X) <-- (pp Z X) (~ (ec (f707408 Z X Y) Z)))
|=============================
|Step 5
|
|? (pp c714193 c714194)
|
|1. (~ (ntpp c714193 c714194))
|2. (~ (ntpp-1 c714194 c714193))
|3. (~ (tpp-1 c714194 c714193))
|4. (pp-1 c714194 c714193)
|
|> ((pp Y X) <-- (pp-1 X Y))
|=============================
|Step 6
|
|? (pp-1 c714194 c714193)
|
|1. (~ (pp c714193 c714194))
|2. (~ (ntpp c714193 c714194))
|3. (~ (ntpp-1 c714194 c714193))
|4. (~ (tpp-1 c714194 c714193))
|5. (pp-1 c714194 c714193)
|
|> hyp
=============================
Step 7

? (~ (ec (f707408 c714193 c714194 Var44) c714193))

1. (~ (ntpp c714193 c714194))
2. (~ (ntpp-1 c714194 c714193))
3. (~ (tpp-1 c714194 c714193))
4. (pp-1 c714194 c714193)

> ((~ (ec X Y)) <-- (pp Y Z) (ec X Z) (~ (tpp Y Z)))
||=============================
||Step 8
||
||? (pp c714193 Var50)
||
||1. (ec (f707408 c714193 c714194 Var44) c714193)
||2. (~ (ntpp c714193 c714194))
||3. (~ (ntpp-1 c714194 c714193))
||4. (~ (tpp-1 c714194 c714193))
||5. (pp-1 c714194 c714193)
||
||> ((pp Y X) <-- (pp-1 X Y))
||=============================
||Step 9
||
||? (pp-1 Var50 c714193)
||
||1. (~ (pp c714193 Var50))
||2. (ec (f707408 c714193 c714194 Var44) c714193)
||3. (~ (ntpp c714193 c714194))
||4. (~ (ntpp-1 c714194 c714193))
||5. (~ (tpp-1 c714194 c714193))
||6. (pp-1 c714194 c714193)
||
||> hyp
|=============================
|Step 10
|
|? (ec (f707408 c714193 c714194 Var44) c714194)
|
|1. (ec (f707408 c714193 c714194 Var44) c714193)
|2. (~ (ntpp c714193 c714194))
|3. (~ (ntpp-1 c714194 c714193))
|4. (~ (tpp-1 c714194 c714193))
|5. (pp-1 c714194 c714193)
|
|> ((ec (f707408 Y Z X) Z) <-- (~ (ntpp Y Z)) (pp Y Z))
||=============================
||Step 11
||
||? (~ (ntpp c714193 c714194))
||
||1. (~ (ec (f707408 c714193 c714194 Var44) c714194))
||2. (ec (f707408 c714193 c714194 Var44) c714193)
||3. (~ (ntpp c714193 c714194))
||4. (~ (ntpp-1 c714194 c714193))
||5. (~ (tpp-1 c714194 c714193))
||6. (pp-1 c714194 c714193)
||
||> hyp
|=============================
|Step 12
|
|? (pp c714193 c714194)
|
|1. (~ (ec (f707408 c714193 c714194 Var44) c714194))
|2. (ec (f707408 c714193 c714194 Var44) c714193)
|3. (~ (ntpp c714193 c714194))
|4. (~ (ntpp-1 c714194 c714193))
|5. (~ (tpp-1 c714194 c714193))
|6. (pp-1 c714194 c714193)
|
|> ((pp Y X) <-- (pp-1 X Y))
|=============================
|Step 13
|
|? (pp-1 c714194 c714193)
|
|1. (~ (pp c714193 c714194))
|2. (~ (ec (f707408 c714193 c714194 Var44) c714194))
|3. (ec (f707408 c714193 c714194 Var44) c714193)
|4. (~ (ntpp c714193 c714194))
|5. (~ (ntpp-1 c714194 c714193))
|6. (~ (tpp-1 c714194 c714193))
|7. (pp-1 c714194 c714193)
|
|> hyp
=============================
Step 14

? (~ (tpp c714193 c714194))

1. (ec (f707408 c714193 c714194 Var44) c714193)
2. (~ (ntpp c714193 c714194))
3. (~ (ntpp-1 c714194 c714193))
4. (~ (tpp-1 c714194 c714193))
5. (pp-1 c714194 c714193)

> ((~ (tpp Y X)) <-- (~ (tpp-1 X Y)))
=============================
Step 15

? (~ (tpp-1 c714194 c714193))

1. (tpp c714193 c714194)
2. (ec (f707408 c714193 c714194 Var44) c714193)
3. (~ (ntpp c714193 c714194))
4. (~ (ntpp-1 c714194 c714193))
5. (~ (tpp-1 c714194 c714193))
6. (pp-1 c714194 c714193)

> hyp


LEMMA

Refine the overlap case from po or pp-1 to po or tpp-1 or ntpp-1.
=============================
Step 1

? (all x (all y (all z (((((ec x y) & (dc y z)) & (c x z)) & (o x z)) => ((po x z) v ((tpp-1 x z) v (ntpp-1 x z)))))))


> revsk
=============================
Step 2

? (((((~ (ec c721250 c721249)) v (~ (dc c721249 c721248))) v (~ (c c721250 c721248))) v (~ (o c721250 c721248))) v ((po c721250 c721248) v ((tpp-1 c721250 c721248) v (ntpp-1 c721250 c721248))))


> hypdisj
=============================
Step 3

? (ntpp-1 c721250 c721248)

1. (~ (tpp-1 c721250 c721248))
2. (~ (po c721250 c721248))
3. (o c721250 c721248)
4. (c c721250 c721248)
5. (dc c721249 c721248)
6. (ec c721250 c721249)

> ((ntpp-1 X Y) <-- (pp-1 X Y) (~ (tpp-1 X Y)))
|=============================
|Step 4
|
|? (pp-1 c721250 c721248)
|
|1. (~ (ntpp-1 c721250 c721248))
|2. (~ (tpp-1 c721250 c721248))
|3. (~ (po c721250 c721248))
|4. (o c721250 c721248)
|5. (c c721250 c721248)
|6. (dc c721249 c721248)
|7. (ec c721250 c721249)
|
|> ((pp-1 Y Z) <-- (ec Y X) (dc X Z) (c Y Z) (o Y Z) (~ (po Y Z)))
|||||=============================
|||||Step 5
|||||
|||||? (ec c721250 Var32)
|||||
|||||1. (~ (pp-1 c721250 c721248))
|||||2. (~ (ntpp-1 c721250 c721248))
|||||3. (~ (tpp-1 c721250 c721248))
|||||4. (~ (po c721250 c721248))
|||||5. (o c721250 c721248)
|||||6. (c c721250 c721248)
|||||7. (dc c721249 c721248)
|||||8. (ec c721250 c721249)
|||||
|||||> hyp
||||=============================
||||Step 6
||||
||||? (dc c721249 c721248)
||||
||||1. (~ (pp-1 c721250 c721248))
||||2. (~ (ntpp-1 c721250 c721248))
||||3. (~ (tpp-1 c721250 c721248))
||||4. (~ (po c721250 c721248))
||||5. (o c721250 c721248)
||||6. (c c721250 c721248)
||||7. (dc c721249 c721248)
||||8. (ec c721250 c721249)
||||
||||> hyp
|||=============================
|||Step 7
|||
|||? (c c721250 c721248)
|||
|||1. (~ (pp-1 c721250 c721248))
|||2. (~ (ntpp-1 c721250 c721248))
|||3. (~ (tpp-1 c721250 c721248))
|||4. (~ (po c721250 c721248))
|||5. (o c721250 c721248)
|||6. (c c721250 c721248)
|||7. (dc c721249 c721248)
|||8. (ec c721250 c721249)
|||
|||> hyp
||=============================
||Step 8
||
||? (o c721250 c721248)
||
||1. (~ (pp-1 c721250 c721248))
||2. (~ (ntpp-1 c721250 c721248))
||3. (~ (tpp-1 c721250 c721248))
||4. (~ (po c721250 c721248))
||5. (o c721250 c721248)
||6. (c c721250 c721248)
||7. (dc c721249 c721248)
||8. (ec c721250 c721249)
||
||> hyp
|=============================
|Step 9
|
|? (~ (po c721250 c721248))
|
|1. (~ (pp-1 c721250 c721248))
|2. (~ (ntpp-1 c721250 c721248))
|3. (~ (tpp-1 c721250 c721248))
|4. (~ (po c721250 c721248))
|5. (o c721250 c721248)
|6. (c c721250 c721248)
|7. (dc c721249 c721248)
|8. (ec c721250 c721249)
|
|> hyp
=============================
Step 10

? (~ (tpp-1 c721250 c721248))

1. (~ (ntpp-1 c721250 c721248))
2. (~ (tpp-1 c721250 c721248))
3. (~ (po c721250 c721248))
4. (o c721250 c721248)
5. (c c721250 c721248)
6. (dc c721249 c721248)
7. (ec c721250 c721249)

> hyp


LEMMA

Combine the mirrored local case splits.
=============================
Step 1

? (all x (all y (all z (((ec x y) & (dc y z)) => (((((dc x z) v (ec x z)) v (po x z)) v (tpp-1 x z)) v (ntpp-1 x z))))))


> revsk
=============================
Step 2

? (((~ (ec c729166 c729165)) v (~ (dc c729165 c729164))) v (((((dc c729166 c729164) v (ec c729166 c729164)) v (po c729166 c729164)) v (tpp-1 c729166 c729164)) v (ntpp-1 c729166 c729164)))


> hypdisj
=============================
Step 3

? (ntpp-1 c729166 c729164)

1. (~ (tpp-1 c729166 c729164))
2. (~ (po c729166 c729164))
3. (~ (ec c729166 c729164))
4. (~ (dc c729166 c729164))
5. (dc c729165 c729164)
6. (ec c729166 c729165)

> ((ntpp-1 Y Z) <-- (ec Y X) (dc X Z) (c Y Z) (o Y Z) (~ (po Y Z)) (~ (tpp-1 Y Z)))
|||||=============================
|||||Step 4
|||||
|||||? (ec c729166 Var35)
|||||
|||||1. (~ (ntpp-1 c729166 c729164))
|||||2. (~ (tpp-1 c729166 c729164))
|||||3. (~ (po c729166 c729164))
|||||4. (~ (ec c729166 c729164))
|||||5. (~ (dc c729166 c729164))
|||||6. (dc c729165 c729164)
|||||7. (ec c729166 c729165)
|||||
|||||> hyp
||||=============================
||||Step 5
||||
||||? (dc c729165 c729164)
||||
||||1. (~ (ntpp-1 c729166 c729164))
||||2. (~ (tpp-1 c729166 c729164))
||||3. (~ (po c729166 c729164))
||||4. (~ (ec c729166 c729164))
||||5. (~ (dc c729166 c729164))
||||6. (dc c729165 c729164)
||||7. (ec c729166 c729165)
||||
||||> hyp
|||=============================
|||Step 6
|||
|||? (c c729166 c729164)
|||
|||1. (~ (ntpp-1 c729166 c729164))
|||2. (~ (tpp-1 c729166 c729164))
|||3. (~ (po c729166 c729164))
|||4. (~ (ec c729166 c729164))
|||5. (~ (dc c729166 c729164))
|||6. (dc c729165 c729164)
|||7. (ec c729166 c729165)
|||
|||> ((c X Y) <-- (~ (dc X Y)))
|||=============================
|||Step 7
|||
|||? (~ (dc c729166 c729164))
|||
|||1. (~ (c c729166 c729164))
|||2. (~ (ntpp-1 c729166 c729164))
|||3. (~ (tpp-1 c729166 c729164))
|||4. (~ (po c729166 c729164))
|||5. (~ (ec c729166 c729164))
|||6. (~ (dc c729166 c729164))
|||7. (dc c729165 c729164)
|||8. (ec c729166 c729165)
|||
|||> hyp
||=============================
||Step 8
||
||? (o c729166 c729164)
||
||1. (~ (ntpp-1 c729166 c729164))
||2. (~ (tpp-1 c729166 c729164))
||3. (~ (po c729166 c729164))
||4. (~ (ec c729166 c729164))
||5. (~ (dc c729166 c729164))
||6. (dc c729165 c729164)
||7. (ec c729166 c729165)
||
||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|||=============================
|||Step 9
|||
|||? (c c729166 c729164)
|||
|||1. (~ (o c729166 c729164))
|||2. (~ (ntpp-1 c729166 c729164))
|||3. (~ (tpp-1 c729166 c729164))
|||4. (~ (po c729166 c729164))
|||5. (~ (ec c729166 c729164))
|||6. (~ (dc c729166 c729164))
|||7. (dc c729165 c729164)
|||8. (ec c729166 c729165)
|||
|||> ((c X Y) <-- (~ (dc X Y)))
|||=============================
|||Step 10
|||
|||? (~ (dc c729166 c729164))
|||
|||1. (~ (c c729166 c729164))
|||2. (~ (o c729166 c729164))
|||3. (~ (ntpp-1 c729166 c729164))
|||4. (~ (tpp-1 c729166 c729164))
|||5. (~ (po c729166 c729164))
|||6. (~ (ec c729166 c729164))
|||7. (~ (dc c729166 c729164))
|||8. (dc c729165 c729164)
|||9. (ec c729166 c729165)
|||
|||> hyp
||=============================
||Step 11
||
||? (~ (ec c729166 c729164))
||
||1. (~ (o c729166 c729164))
||2. (~ (ntpp-1 c729166 c729164))
||3. (~ (tpp-1 c729166 c729164))
||4. (~ (po c729166 c729164))
||5. (~ (ec c729166 c729164))
||6. (~ (dc c729166 c729164))
||7. (dc c729165 c729164)
||8. (ec c729166 c729165)
||
||> hyp
|=============================
|Step 12
|
|? (~ (po c729166 c729164))
|
|1. (~ (ntpp-1 c729166 c729164))
|2. (~ (tpp-1 c729166 c729164))
|3. (~ (po c729166 c729164))
|4. (~ (ec c729166 c729164))
|5. (~ (dc c729166 c729164))
|6. (dc c729165 c729164)
|7. (ec c729166 c729165)
|
|> hyp
=============================
Step 13

? (~ (tpp-1 c729166 c729164))

1. (~ (ntpp-1 c729166 c729164))
2. (~ (tpp-1 c729166 c729164))
3. (~ (po c729166 c729164))
4. (~ (ec c729166 c729164))
5. (~ (dc c729166 c729164))
6. (dc c729165 c729164)
7. (ec c729166 c729165)

> hyp
